計算可能性 (computability)
計算可能関数 - Wikipedia
Curry-Howard 對應
カリー=ハワード同型対応 - Wikipedia
計算可能関数 - Wikipedia
Curry-Howard 對應
カリー=ハワード同型対応 - Wikipedia
non-classical logic、non-standard logic、非古典論理
古典論理を含む、非古典論理やその他論理の集藏。それぞれに似た體系がいっぱい有る旨を注意
Category:論理学 - Wikipedia
Category:Logic - Wikipedia
證明支援
Curry-Howard 對應
Rocq (a.k.a. Coq)
Welcome! | The Coq Proof Assistant
Extraction of programs in OCaml and Haskell — Coq 8.10.2 documentation
type theory
型理論 - Wikipedia
Type theory - Wikipedia
Type Theory (Stanford Encyclopedia of Philosophy)
intuitionistic logic。constructive logic
直観主義論理 - Wikipedia
Intuitionistic logic - Wikipedia